#include "CTLLexer.hh"
#include <iostream>

CTLLexer::CTLLexer (std::string		formula)
  : formula_ (formula),
    offset_ (0),
    vars_ (),
    offset_var_ (0)
{
}

bool
CTLLexer::isNextToken (std::string	test)
{
  unsigned j = 0;
  for (unsigned i = 0; i < test.length (); ++i, ++j)
    {
      while (formula_[offset_ + j] == ' ')
	++j;

      if (formula_[offset_ + j] != test[i])
	return false;
    }

  offset_ += j;

  return true;
}

bool
CTLLexer::eof ()
{
  return (offset_ >= formula_.length ());
}

unsigned
CTLLexer::getOffset ()
{
  return offset_;
}


void
CTLLexer::pushNextVar ()
{
  for (; formula_[offset_] == ' '; ++offset_)
    ;
  unsigned i = offset_;
  for (; formula_[offset_ ] != ' ' && formula_[offset_] != ',' && formula_[offset_] != ')' && offset_ < formula_.length (); ++offset_)
    ;
  std::string var = formula_.substr (i, offset_ -  i);
  vars_.push_back (var);
}

std::string
CTLLexer::getNextVar ()
{
  return vars_[offset_var_++];
}

symbols
CTLLexer::getNextToken ()
{
  // std::cout << offset_ << std::endl;
  // std::cout << formula_ << std::endl;

  if (isNextToken ("AND") || isNextToken ("and"))
    return AND;

  if (isNextToken ("OR") || isNextToken ("or"))
    return OR;

  if (isNextToken ("NOT") || isNextToken ("not"))
    return (NOT);

  if (isNextToken ("IMPLIES") || isNextToken ("implies"))
    return (IMPLIES);

  if (isNextToken ("AX") || isNextToken ("ax"))
    return (AX);

  if (isNextToken ("EX") || isNextToken ("ex"))
    return (EX);

  if (isNextToken ("AF") || isNextToken ("af"))
    return (AF);

  if (isNextToken ("EF") || isNextToken ("ef"))
    return (EF);

  if (isNextToken ("AG") || isNextToken ("ag"))
    return (AG);

  if (isNextToken ("EG") || isNextToken ("eg"))
    return (EG);

  if (isNextToken ("AU") || isNextToken ("au"))
    return (AU);

  if (isNextToken ("EU") || isNextToken ("eu"))
    return (EU);

  if (isNextToken ("true") || isNextToken ("TRUE"))
    return (T);

  if (isNextToken ("false") || isNextToken ("FALSE"))
    return (F);

  if (isNextToken ("("))
    return (LPAR);

  if (isNextToken (")"))
    return (RPAR);

  if (isNextToken (","))
    return (COMMA);

  pushNextVar ();
  return VAR;
}
